Inference at * 1 
Iof proof for Lemma Agatha Murder Puzzle (JProver)Lori2R:


1. Agatha hates Charles
2. Agatha hates Agatha
3. p:Person. p is richer than Agatha  The Butler hates p
4. p:Person. Agatha hates p  Charles hates p
5. p:Person. Agatha hates p  The Butler hates p
6. p:Person. p hates Agatha  p hates The Butler  p hates Charles
7. p, q:Person. p kills q  p is richer than q
8. p, q:Person. p kills q  p hates q
  The Butler kills Agatha & Charles kills Agatha 

latex

 by * JproverR 

latex

 .

Definitions

P  Q, left+right, x is richer than y, False, P & Q, A, x kills y, x:AB(x), P  Q, x:A. B(x), x:AB(x)